\documentclass[a4paper,10pt]{article}
\usepackage[utf8]{inputenc}

\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{amstext, amssymb, amsfonts, amsmath}
%\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{geometry}
\usepackage{enumerate}
\usepackage{times}
\usepackage{color}
\usepackage{url}
\usepackage{hyperref}


\usepackage{macron}
\usepackage{typecasemacro}

%opening
\title{Enhanced process abstractions for \\ runtime session adaptation}
\author{Cinzia Di Giusto \and Jorge A. Pérez}
\date{Short Report for a BETTY STSM (COST-STSM-IC1201-14835) \\ 
Lisbon, August 2013}

\begin{document}

\maketitle



     
\begin{abstract}
During the STSM, we defined the bases  of 
a novel formal architectural framework for specifying and reasoning about \emph{robust} com\-mu\-ni\-ca\-tion-centric systems, specified 
as $\pi$-calculus processes and disciplined via session types. The intended framework is meant to 
modularly isolate
the communication part of the system
from the program components handling runtime adaptation requests, which may come from inside the system or from external requirements.
This should be beneficial for obtaining more clear specifications, possibly enabling also reuse of existing session types theories.
We choose an event-based approach to connect behavioral and reconfiguration components in an uniform way.
In this short note, we give a high-level description of the framework and comment on some technical details.
%A significant advantage of adopting our framework is that it allows reuse of existing behavioral type disciplines for correct communications,
%treating error handling and recovery as an orthogonal issue. To illustrate our conceptual framework, we consider a number of exceptional circumstances that may occur at runtime, ranging from application migration until rollback, and describe how they are 
%handled in our setting.
\end{abstract}
%
%\section{Suggestions}
%%The abstract can be much shorter and more general. 
%
%Mention the well-known work on exceptions for binary session types, and other session disciplines with buffers/queues~\cite{DBLP:journals/jfp/GayV10}.
%
%Before giving technical details, it would be very useful to give a concrete example for configurations/networks, and their evolution.
%The example could illustrate records, memories, etc. 





\section{STSM objectives and results}
During the one week STSM in Lisbon we explored flexible mechanisms for statically controlling reconfiguration events in models of communication-centric applications. A motivating observation is that separating the session protocols from the mechanisms that may affect their control structures (such as, e.g., exception handling constructs~\cite{DBLP:conf/concur/CarboneHY08}) may turn useful to obtain simpler process specifications and more effective static verification techniques. 

\paragraph{Description of the work carried out during the STSM.}
The main outcome of the STSM is a conceptual framework for ``supervising'' session-based applications.
%We discussed a framework to support the construction of controlling tools for session languages. 
Our proposal is able to respond to exceptional circumstances detected on already established sessions.
Such circumstances may include physical problems (such as, e.g., the failure of a connection) as well as logical issues (such as, e.g., the inconsistency of the data received, based on conditions not expressible via types). 
Drawing inspiration from~\cite{Kouzapas12}, a novelty is that the detection of these runtime issues follows an \emph{event-based approach}: this brings modularity into specifications as it allows us to treat control structures independently from the specific process constructs. 
% and allows us to treat internal and external circumstances in a uniform way. 
%We feel that our proposal is conceptual rather than technical: our event-based approach to reconfiguration is independent from specific process constructs.
 This is advantageous also because existing session-typed frameworks may be reused and/or adapted to our scenario. 
For the sake of simplicity,  we chose to work with a synchronous session language \cite{DBLP:journals/entcs/YoshidaV07,DBLP:conf/sac/GiustoP13}.

\paragraph{Description of the main results obtained.}
%As a motivating example, consider a simple client/server scenario. 
%In this example we have two actors: the client and the server both with their own code that manages the interaction between the two actors. 
In our framework, a system is modeled as a \emph{network}, i.e, a collection of \emph{configurations}, each of which represents a participant of the system. More in general, each configuration is implemented as a separate unit with name $l$  which contains the code (i.e., the session protocol), the controlling system, and a state. Configurations are denoted with $\tuplem{l}{P}{S}$, where $P$  stands for the composition of the code and the controlling system,  $S$ is the state and $l$ is the name of the configuration. We now explain these elements separately:

\begin{itemize}
\item The state of a configuration $S$ is given by  a number of \emph{records}: each record is associated to an established connection. Records store  information on the current type of the session, together with a queue of special messages that are handled by the controlling system.
As we choose to work with synchronous sessions, our records are simple; in an asynchronous setting they may be used as the buffers or queues upon which communication typically relies (as in, for instance,~\cite{DBLP:journals/jfp/GayV10,Kouzapas12}).

\item The controlling system is a  \emph{handler} that depending on some external or internal signals/events takes some decisions on the behavior of the configuration. Intuitively, the handler is able to interact with an unspecified environment that can send distinguished messages; these messages  may refer to internal (to the configuration) or external events. For instance, the environment could send a special signal whenever something unexpected happens (e.g. the connection between two participants has failed).
Based on the information collected from the environment and on the internal state of the configuration, the handler will take a certain sequence of actions. To this end, 
following the approach in~\cite{Kouzapas12},
we rely on a typecase operator: by testing the current type of the session (stored in a given record), the handler may base its decision not only on external messages but also on the specific nature of the session (i.e., its typestate).
\end{itemize}


What is a proper reconfiguration policy in a session-typed setting? We explored two main possibility.
A first, simple policy would be to interrupt all the established communications of the configuration, remove their associated structures (say, queues for the endpoints), and to restart all involved protocols. While somewhat drastic, this policy is adopted in practice, for instance in the supervision trees provided by the Erlang language \cite{erlang:sup}. Nevertheless, less disruptive policies, enforcing local recovery actions, are often desirable. 
%This is obviously a very restrictive and drastic decision as we are influencing also sessions that could have been independent from the session in which the problem was detected. 
To that end, we need to
%Nevertheless, in order to treat more complex scenarios we need to 
enrich our configurations with data structures that store information on how sessions depend from each other, as well as with information that allows us to implement rollback policies, thus giving the possibility to the handler to restore previous/old configurations.

More concretely, we discussed an extension of configurations with a new component, a structure that we call \emph{memory}.
Extended configurations are denoted $\tuple{l}{P}{S}{M}$, where memory $M$ is a tree of objects. Each of these objects represents a check or recovery point, consisting of a portion of code with its associated state. Intuitively, we create a node in the tree every time we establish a new session; the tree structure thus captures the dependencies between sessions, and each node stores the information needed to restart the computation from that point in case something unexpected occurs. 
In such a case, the handler implements the appropriate recovery strategy, depending on the message received and on the state, and exploiting the information that can be retrieved from the memory.
These recovering techniques are reminiscent of those used in works on exception handling~ \cite{DBLP:conf/concur/CarboneHY08} and on reversible models~\cite{DBLP:conf/concur/DanosK04,DBLP:conf/concur/LaneseMS10}.

Overall, during the STSM we explored a number of design decisions, some of which are contained in the previous high-level description.
We discussed the role of the session language in our conceptual framework and how to distill the key components for recovery present in existing proposals.
%took some design decision, such as type of session to work with,discussing what would be the role of the manager and 
We also worked out coarsely the details of the syntax and semantics for our proposal. 

\section{Some technical details}

\paragraph{Syntax.} We give here more precise details on how to handle configurations without memory. The treatment of memory is left for future work. 
Table \ref{tab:all} shows the syntax of the framework introduced above. Next we give some explanations and intuitions on the semantics.


\begin{table}[ht]
$$
\begin{array}{ll}
\text{Network} & N::= \nil \mid C \parallel C \mid \nu \til{\kappa}~ C \\

\text{Configuration:}  &  C :: = \tuplem{l}{P}{S} \\

\text{Process:} &  P::=       \nil \mid  \local{\til{\kappa}}{R} \mid \manager \mid P | P  \\
\text{Manager:} & 
\manager ::= \queue{\kappa^p}{\msg} \mid \interrupt \mid \case{\kappa}{\msg}{\manager} \dots \\  
\text{State:} & S ::= \emptyset \mid \state{\kappa^p}{T^{\til{\kappa}}}{q},S\\

\text{Queue:} & q::=\varepsilon \mid q \cdot \msg  \\

\text{Messages:} & \msg ::=  \mstop \mid \dots \\

 \end{array}
$$
\caption{Framework syntax} \label{tab:all}
\end{table}


The main concepts are \emph{networks} and \emph{configurations}. Each network models the idea of a set of running units that interact together by establishing sessions and by exchanging messages. Each unit has a single task and it is implemented by a configuration. This way we could have units that models a client behavior, other that are servers, etc.
More formally,  a network ranged over by $N, M, \dots $is the restriction on a number of channels $\til{\kappa}$ of the parallel composition of a set of configurations. 
A configuration (ranged over by $C, D, \dots$) located at $l$ is denoted 
$ \tuplem{l}{P}{S}$ and is 
composed by two parts: a process $P$ that implements the actual task of the unit (its session behavior), together with some management procedures and  a state $S$ that stores information on the session channels used by the configuration.
The intuition behind configurations is that of a process that runs independently establishing sessions either internally or with other configurations/units.  
An internal session represents a task that is implemented internally to the same unit: i.e., both endpoints belong to the same configuration. An external session is represented by the interaction of two configurations: for instance one configuration plays the role of a server offering certain services while the other is a client requesting one of those services. 
Inside configurations the manager or handler is able to detect problematic/error situations and to handle them. In this simple scenario, it can only communicate via partner sessions by enqueuing  special messages, or stop the current computation via the command $\mstop$.
Hence,  a process is the parallel composition of a handler $\manager$ and a number of running items (that represent the code of the unit) $\local{\til{\kappa}}{R}$, where $R$ is a process given in the session language in Table \ref{tab:sessionlan} and $\til{\kappa}$ is the nesting of established sessions in $R$.

 Finally, $S$ is a collection of records $\state{\kappa^p}{T}{q}$ where $\kappa^p$ is the name of the channel with its polarity\footnote{It is necessary to store the polarity as we could have both ends of the channel in the same configuration (internal session).}, $T$ is the ``runtime'' type of the session in $\kappa$, and $q$ is a queue where we store special messages  $\msg$ that are sent by  $\manager$ via the $\queue{\kappa^p}{\msg}$ operator  and that are used to perform management actions on the session $\kappa^p$.  



\begin{table}[t]
 $$
\begin{array}{lrlr}
R & ::=  &   \request{a}{x:T}.R  & \text{session request}	\\
	& \sepr &   \accept{a}{x:T}.P  & \text{session acceptance: linear}	\\
	       & \sepr & \raccept{a}{x:T}.P  & \text{session acceptance: persistent}	\\
	& \sepr &  \outC{k}{\tilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\tilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{k'}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    	&\sepr&   \branch{k}{n_1{:}P_1 \parallel \cdots \parallel n_m{:}P_m} & \text{branching}\\
  %	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{arithmetic expressions}
\end{array} 
$$
 \caption{Syntax for sessions}\label{tab:sessionlan}
\end{table}


\paragraph{Semantics.}
As hinted at above, our configurations manage both internal and external sessions, this way we need to duplicate the semantics of each operator into a global semantics (Table \ref{tab:globsem}) that refers to sessions established between two configurations and a local semantics (Table \ref{tab:localsem}) that deals with internal sessions (i.e. sessions established within the configuration).
We explain in detail only the case of the global semantics, the local semantics is analogous.

\begin{table}[ht]
$$
\begin{array}{ll}
  \rulename{r:Open} &
 \tuplem{l}{\local{\til{\kappa_1}}{\accept{a}{x:T}.P_1}}{S_1} \parallel 
  \tuplem{n}{\local{\til{\kappa_2}}{\request{a}{y:\overline{T}}.P_2}}{S_2}
 \pired   \\ &
 \quad \nu \kappa~ ( 
 \tuplem{l}
  {\local{\til{\kappa_1}\cdot \kappa^+}{P_1\subst{\kappa^+}{x}}}
  {S_1, \state{\kappa^+}{T}{\varepsilon}}
   \parallel  \tuplem{n}
   {\local{\til{\kappa_2}\cdot \kappa^-}{P_2\subst{\kappa^-}{y}}}
   {S_2, \state{\kappa^-}{\overline{T}}{\varepsilon}} )\\
\\

   \rulename{r:I/O} &
\tuplem{l}{\local{\til{\iota_1}}{\outC{\cha^{p}}{\tilde{e}}.P_1}}{S_1, \state{\kappa^p}{!(\tilde{\capab}).\alpha}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_2}}
{S_2, 
\state{\kappa^{\overline{p}}}{?(\tilde{\capab}).\overline{\alpha}}{q_2}}
 \pired 
\\& \qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_1}}{S_1, \state{\kappa^p}{\alpha}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{P_2\subst{\til{e}}{\til{x}}}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha}}{q_2}} \quad (\kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\

 \rulename{r:Pass} &
\tuplem{l}
{\local{\til{\iota_1}}{\throw{\cha_1^{p}}{\kappa_2}.P_1}}{S_1, \state{\kappa_1^p}{!\beta.\alpha}{q_1}, \state{\kappa_2}{\beta}{q_1'}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{\catch{\cha_1^{\overline{p}}}{x}.P_2}}
{S_2, 
\state{\kappa_1^{\overline{p}}}{?\beta.\overline{\alpha}}{q_2}}
 \pired 
\\ &\qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_1}}{S_1, \state{\kappa_1^p}{\alpha}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}\cdot \kappa_2}{P_2\subst{\kappa_2}{x}}}
{S_2, 
\state{\kappa_1^{\overline{p}}}{\overline{\alpha}}{q_2},
 \state{\kappa_2}{\beta}{q_1'}} \quad (\kappa_1^p \in \iota_1 \text{ and } \kappa_1^{\overline{p}} \in \iota_2)
\\ 

\\

 \rulename{r:Sel} &
\tuplem{l}
{\local{\til{\iota_1}}{\branch{\cha^{p}}{h_1{:}P_1 \parallel \cdots \parallel h_m{:}P_m}}}
{S_1, \state{\kappa^p}{ \&\{h_1:\alpha_1, \dots,  h_m:\ST_m \}}{q_1}} \parallel \\ &

\tuplem{n}
{\local{\til{\iota_2}}{\select{\cha^{\overline{p}}}{h_j};Q}}
{S_2, 
\state{\kappa^{\overline{p}}}{\oplus\{h_1:\overline{\alpha_1}, \dots , h_m:\overline{\ST_m} \} }{q_2}}
 \pired 
\\& \qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_j}}{S_1, \state{\kappa^p}{\alpha_j}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{Q}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha_j}}{q_2}}
 \quad  (1 \leq j \leq m,~  \kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\
 \rulename{r:Close} & 
\tuplem{l}{\local{\til{\iota_1}}{\close{\cha^{p}}.P_1}}{S_1, \state{\kappa^p}{\varepsilon}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{\close{\cha^{\overline{p}}}.P_2}}
{S_2, 
\state{\kappa^{\overline{p}}}{\varepsilon}{q_2}}
  \pired 
\\ & \qquad
\tuplem{l}{\local{\til{\iota_1}}{P_1}}{S_1} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{P_2}}
{S_2} \quad (\kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)   
   \end{array}
$$

 
 \caption{Global semantics} \label{tab:globsem}
\end{table}



We start with session establishment: upon session establishment, as in standard session languages, we create a fresh channel $\kappa$ and assign one end of the channel to each configuration. On each configuration, we update each unit adding the name of the channel of the session $\local{\til{\kappa_1}\cdot \kappa^+}{\cdot}$ and  $\local{\til{\kappa_2}\cdot \kappa^-}{\cdot}$. Then in each of the states $S_1$ and $S_2$, we add  a new state $\state{\kappa^+}{T}{\varepsilon}$ ($\state{\kappa^-}{\overline{T}}{\varepsilon}$ respectively) where $T$ is the type of the session in $\kappa^+$ and $\varepsilon$ in an empty queue. Conversely the operator $\close{}$  ends the communication and therefore eliminates the corresponding record in the state. Input/output  and selection operators are standard. We just comment on rule \rulename{r:Pass}. When a channel $\kappa_2$ is communicated along $\kappa_1^p$, non only the channel but also its record is moved to the configuration containing $\kappa^{\overline{p}}$.

In addition to common rules for session establishment and communication, we need few rules to define the behavior of the handler. These rules are contained in Table \ref{tab:handlersem}.
The first two rules show the semantics of the $\queue{\kappa}{msg}$ operator. The operator is used to add a message $msg$ in the corresponding queue of the session channel $\kappa$. The two rules distinguish the case in which the channel is internal (i.e., it belongs to the state of the same configuration of the handler) or external (i.e., it appears in the state of another configuration). The operator $\interrupt$  instead destroys all states and sends a stop message to all the communication partners. Notice that the destruction of a record in the state implies that the session established on the corresponding channel has failed and no more operation can be done on the session.
\begin{table}[t]

$$
\begin{array}{ll}
  \rulename{r:Open} &
 \tuplem{l}
{\local{\til{\kappa_1}}{\accept{a}{x:T}.P_1} \mid 
  \local{\til{\kappa_2}}{\request{a}{y:\overline{T}}.P_2}
}{S}  \pired   \\ &
 \ \nu \kappa  
 \tuplem{l} 
  {\local{\til{\kappa_1}\cdot \kappa^+}{P_1\subst{\kappa^+}{x}} \mid 
\local{\til{\kappa_2}\cdot \kappa^-}{P_2\subst{\kappa^-}{y}}} 
  {S, \state{\kappa^+}{T}{\varepsilon},
        \state{\kappa^-}{\overline{T}}{\varepsilon}}\\

  \\
\\
 \rulename{r:Queue} &
\tuplem{l}
 {\queue{\kappa^p}{\msg}.P}
 {S,\state{\kappa^p}{T}{q}}
 
\pired 
\tuplem{l}
 {P}
 {S,\state{\kappa^p}{T}{q \cdot \msg}}\\

 \\
   \rulename{r:I/O} &
\tuplem{l}{\local{\til{\iota_1}}{\outC{\cha^{p}}{\tilde{e}}.P_1} \mid \local{\til{\iota_2}}{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_2} }
          {S, \state{\kappa^p}{!(\tilde{\capab}).\alpha}{q_1}, \state{\kappa^{\overline{p}}}{?(\tilde{\capab}).\overline{\alpha}}{q_2}} \parallel 
 \pired 
\\& \qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_1} \mid \local{\til{\iota_2}}{P_2\subst{\til{e}}{\til{x}}}}{S_1, \state{\kappa^p}{\alpha}{q_1},\state{\kappa^{\overline{p}}}{\overline{\alpha}}{q_2}}  \quad (\kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\

 \rulename{r:Pass} &
\tuplem{l}
{\local{\til{\iota_1}}{\throw{\cha_1^{p}}{\kappa_2}.P_1} \mid \local{\til{\iota_2}}{\catch{\cha_1^{\overline{p}}}{x}.P_2}}{S_1, \state{\kappa_1^p}{!\beta.\alpha}{q_1}, \state{\kappa_2}{\beta}{q_1'}, \state{\kappa_1^{\overline{p}}}{?\beta.\overline{\alpha}}{q_2}}
 \pired 
\\ &\qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_1} \mid \local{\til{\iota_2}\cdot \kappa_2}{P_2\subst{\kappa_2}{x}}}{S_1, \state{\kappa_1^p}{\alpha}{q_1}, \state{\kappa_1^{\overline{p}}}{\overline{\alpha}}{q_2},
 \state{\kappa_2}{\beta}{q_1'}} \quad (\kappa_1^p \in \iota_1 \text{ and } \kappa_1^{\overline{p}} \in \iota_2)
\\ 

\\

 \rulename{r:Sel} &
\tuplem{l}
{\local{\til{\iota_1}}{\branch{\cha^{p}}{h_1{:}P_1 \parallel \cdots \parallel h_m{:}P_m}} \mid \local{\til{\iota_2}}{\select{\cha^{\overline{p}}}{h_j};Q}}
{\\ & \ S_1, \state{\kappa^p}{ \&\{h_1:\alpha_1, \dots,  h_m:\ST_m \}}{q_1}, \state{\kappa^{\overline{p}}}{\oplus\{h_1:\overline{\alpha_1}, \dots , h_m:\overline{\ST_m} \} }{q_2}} 
 \pired 
\\& \qquad 
\tuplem{l}{\local{\til{\iota_1}}{P_j}}{S_1, \state{\kappa^p}{\alpha_j}{q_1}} \parallel 
\tuplem{n}
{\local{\til{\iota_2}}{Q}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha_j}}{q_2}}
 \quad  (1 \leq j \leq m,~  \kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\
 \rulename{r:Close} & 
\tuplem{l}{\local{\til{\iota_1}}{\close{\cha^{p}}.P_1}\mid \local{\til{\iota_2}}{\close{\cha^{\overline{p}}}.P_2}}{S_1, \state{\kappa^p}{\varepsilon}{q_1},\state{\kappa^{\overline{p}}}{\varepsilon}{q_2}} 
  \pired 
\\ & \qquad
\tuplem{l}{\local{\til{\iota_1}}{P_1} \mid \local{\til{\iota_2}}{P_2}}{S_1}  \quad (\kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)   

\end{array}
$$
 
 \caption{Local semantics} \label{tab:localsem}
\end{table}





\begin{table}[t]

$$
\begin{array}{ll}
  
 \rulename{r:QueueL } &
\tuplem{l}
 {\queue{\kappa^p}{\msg}}
 {S,\state{\kappa^p}{T}{q}}
\pired 
\tuplem{l}
 {\nil}
 {S,\state{\kappa^p}{T}{q \cdot \msg}}\\
\\
\rulename{r:QueueG} &
\tuplem{l}
 {\queue{\kappa^p}{\msg}}
 {S_1} \parallel \tuplem{n}
 {P}
 {S_2,\state{\kappa^p}{T}{q} } 
\pired 
\tuplem{l}
 {\nil}
 {S_1}  \parallel \tuplem{n}
 {P}
 {S_2,\state{\kappa^p}{T}{q\cdot \msg} }\\
\\
 \rulename{r:Stop} &
\tuplem{l}
 {\interrupt}
 {\state{\kappa_1^{p_1}}{T_1}{q_1} \dots \state{\kappa_n^{p_n}}{T_n}{q_n}}
\pired 
\tuplem{l}
 {\prod_{i\in [1..n]} \queue{\kappa_i^{\overline{p_i}}}{\mstop}}
 {\emptyset}

\end{array}
$$
 
 \caption{Handler semantics} \label{tab:handlersem}
 
\end{table}









\paragraph{Structural congruence rules and compositional rules.}
Finally Table \ref{tab:parall} handles parallel composition, and Table \ref{tab:structcong} contains laws for defining structural congruence.
 
\begin{table}[th!]

$$
\begin{array}{c}
 \cfrac
{\tuplem{l}{P}{S} \pired \tuplem{l}{P'}{S'}}
{\tuplem{l}{P|Q}{S} \pired \tuplem{l}{P'|Q}{S'}} \\
\\
\cfrac
{\tuplem{l}{P_1}{S_1} \pired \tuplem{l}{P_1'}{S_1'}}
{\tuplem{l}{P_1}{S_1} \parallel \tuplem{n}{P_2}{S_2} \pired \tuplem{l}{P_1'}{S_1'}\parallel \tuplem{n}{P_2}{S_2}} \\
\\
\cfrac
{N \pired N'}
{\nu \kappa N \pired \nu \kappa N'}
\\
\\
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q

\end{array}
$$
\caption{Parallel composition} \label{tab:parall}
\end{table}

\begin{table}[ht]
$$
\begin{array}{ll}
 !a(x).P \equiv !a(x).P | a(x).P &
\local{\til{\kappa}}{P | Q} \equiv \local{\til{\kappa}}{P } | \local{\til{\kappa}}{ Q}\\
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\cha}{\nil} \!\equiv\! \nil & \restr{\cha}{\restr{\kappa'}{P}} \!\equiv\! \restr{\cha'}{\restr{\cha}{P}} \\
\restr{\cha}{C} \!\para \! D \!\equiv\! \restr{\cha}{(C \!\para \! D)} ~~\text{(if $\cha \not\in \mathsf{fc}(D)$)}
\end{array}
$$
\caption{Structural congruence laws} \label{tab:structcong}
\end{table}


\section{Example}
Consider the case of a holiday booking service, in which we have a coordinator server (i.e. the travel agency) that manages all the necessary steps to provide its clients complete holidays, in addition we have a number of servers each dealing with a specific aspect of the holiday (traveling, hosting, special treatments, etc.).  
We assume to work with four actors: a client, a coordinator server, a travel and a hotel server. Hence our network is composed by four configurations. 
In our example, the client after having sent some personal data to the travel agency coordinator, is repeatedly asking for a package (travel + hotel) until she is satisfied and proceeds with the payment. On the coordinator side, the coordinator asks for a suitable travel  and hotel options to the two subservers until it receives a positive confirmation from the client.
Notice that as soon as a session is established, the corresponding handler is instantiated with the name of the session. 
In this example, all handlers are built in the same way: i.e., they recursively check if a new message has been added to the queue of the channel $\kappa$. In this simple modelization we could only receive stop messages, if this is the case, the handler interrupts the current session.


$$
\begin{array}{ll}
\text{Network: } & \tuplem{c}{Client}{\emptyset} \parallel \tuplem{cs}{Coordinator}{\emptyset} \parallel \tuplem{t}{Travel}{\emptyset} \parallel  \tuplem{h}{Hotel}{\emptyset} \\ 
 \text{Client:}& \request{v}{k_v:\overline{T_v}}.(handler(k_v) \mid \outC{k_v}{data}.rec~ X.(\inC{k_v}{sol}.\select{k_v}{agreeon(sol)};\\ & \branch{k_v}{yes: \outC{pay}.\close{k_v} \parallel no: X})) \\
\text{Coordinator:}& !\accept{v}{k_v:T_v}.(handler(k_v) \mid \inC{k_v}{data}.\\
 & rec ~ X. ( \request{t}{k_t:\overline{T_t}}. (handler(k_t) \mid \outC{k_t}{data}.\inC{k_t}{sol1}.\close{k_t}. \\
 & \request{h}{k_h:\overline{T_h}}.(handler(k_h) \mid \outC{k_h}{data}.\inC{k_h}{sol2}.\close{k_t}.\\
 & \outC{k_h}{sol1, sol2}.\branch{k_h}{yes : \select{k_h}{yes}; \inC{k_h}{pay}.\close{k_h} \parallel no : \select{k_h}{no};X} ))))\\
\text{Travel:}& !\accept{t}{k_t:T_t}.(handler(k_v) \mid \inC{k_t}{x}.\outC{k_t}{sol}.\close{k_t} \\
\text{Hotel:}& !\accept{h}{k_h:T_h}.\inC{k_h}{x}.\outC{k_h}{sol}.\close{k_h})\\
handler(k): & rec ~X. \mathsf{case} ~ k ~ \mathsf{of}~ \mstop: ~\interrupt ;  \\
& \qquad \qquad  \qquad \ \  \mathsf{otherwise}: ~X 
\end{array}
$$


\section{Future collaboration and foreseen publication with host institution }
The aim of the STSM in Lisbon was to put the basis for a new framework where aspects connected to session recovery and adaptation could be handled in a modular and uniform way.
In this short report we have shown a first step towards this objective, this report shows how  the modular construction works and gives some ideas on how the rest of the project will be carried on. 
Our goal is now to extend this framework so to be able to treat  memories and therefore be able to have more expressive handlers (e.g. handlers that can support recover and rollback functions). The design of the framework  will then be finalized with the construction of a suitable typing system that should be used to show the consistency of sessions communication in this new framework. 
Ongoing work proceeds by remote discussions in which we are converging towards concrete technical details; we expect to produce a technical report in the following weeks: such a report should be the basis for a forthcoming conference submission, such as for instance
CONCUR'14 (the 25th Conference on Concurrency Theory) or DISCOTEC'14 (the 9th International Federated Conference on Distributed Computing Techniques) . 


\bibliographystyle{abbrv}
\bibliography{referen}
\end{document}

The report should contain the following information:
- purpose of the STSM;
- description of the work carried out during the STSM;
- description of the main results obtained;
- future collaboration with host institution (if applicable);
- foreseen publications/articles resulting or to result from the STSM (if applicable);
- confirmation by the host institution of the successful execution of the STSM;
- other comments (if any).


